package tr.edu.ege.kipler.satisfiability.syntactical;

import tr.edu.ege.kipler.syntax.BinaryBooleanExpression;
import tr.edu.ege.kipler.syntax.ModalExpression;
import tr.edu.ege.kipler.syntax.WorldElement;
import tr.edu.ege.kipler.syntax.WorldElementVisitor;
import tr.edu.ege.kipler.syntax.atomicformula.ConceptAssertion;
import tr.edu.ege.kipler.syntax.atomicformula.ConceptDefinition;
import tr.edu.ege.kipler.syntax.atomicformula.ObjectRoleAssertion;
import tr.edu.ege.kipler.syntax.atomicformula.RoleAssertion;
import tr.edu.ege.kipler.syntax.atomicformula.RoleInclusion;
import tr.edu.ege.kipler.syntax.atomicformula.SameIndividualAssertion;
import tr.edu.ege.kipler.syntax.atomicformula.ConceptDefinition.Type;
import tr.edu.ege.kipler.syntax.concept.BinaryConcept;
import tr.edu.ege.kipler.syntax.concept.Concept;
import tr.edu.ege.kipler.syntax.concept.ConceptName;
import tr.edu.ege.kipler.syntax.concept.BinaryConcept.Constructor;

/**
 * 
 * @author İnanç Seylan
 *
 */
public class TopConsistenceNormalFormVisitor implements WorldElementVisitor {
	private WorldElement normalForm;

	public WorldElement getNormalForm() {
		return normalForm;
	}

	public void visitConceptAssertion(ConceptAssertion ca) {
		// Nothing to do
		normalForm = ca;
	}

	public void visitConceptDefinition(ConceptDefinition cd) {
		try {
			if (cd.getType() == ConceptDefinition.Type.PRIMITIVE) {
				normalForm = primitiveConceptDefinition(cd);
			} else if (cd.getType() == ConceptDefinition.Type.NON_PRIMITIVE) {
				normalForm = nonPrimitiveConceptDefinition(cd);
			}
		} catch (CloneNotSupportedException e) {
			// TODO Auto-generated catch block
			e.printStackTrace();
		}
	}

	public void visitObjectRoleAssertion(ObjectRoleAssertion ra) {
		// Nothing to do
		normalForm = ra;
	}

	public void visitBinaryElement(BinaryBooleanExpression be) {
		TopConsistenceNormalFormVisitor visitor = new TopConsistenceNormalFormVisitor();
		be.getLhs().accept(visitor);
		be.setLhs(visitor.getNormalForm());
		visitor = new TopConsistenceNormalFormVisitor();
		be.getRhs().accept(visitor);
		be.setRhs(visitor.getNormalForm());
		normalForm = be;
	}

	public void visitModalElement(ModalExpression me) {
		TopConsistenceNormalFormVisitor visitor = new TopConsistenceNormalFormVisitor();
		me.getExpression().accept(visitor);
		me.setExpression(visitor.getNormalForm());
		normalForm = me;
	}

	public void visitRoleAssertion(RoleAssertion ra) {
		// Nothing to do
		normalForm = ra;
	}

	public void visitRoleInclusion(RoleInclusion ri) {
		// Nothing to do
		normalForm = ri;
	}

	public void visitSameIndividualAssertion(SameIndividualAssertion ia) {
		// Nothing to do
		normalForm = ia;
	}

	private ConceptDefinition nonPrimitiveConceptDefinition(ConceptDefinition cd)
			throws CloneNotSupportedException {
		Concept C = cd.getLhs();
		Concept D = cd.getRhs();
		Concept negC = cd.getLhs().copy().toggleNegated();
		Concept negD = cd.getRhs().copy().toggleNegated();
		BinaryConcept lhs = new BinaryConcept(Constructor.UNION, negC,
				D);
		BinaryConcept rhs = new BinaryConcept(Constructor.UNION, negD,
				C);
		ConceptDefinition result = new ConceptDefinition(Type.NON_PRIMITIVE,
				new BinaryConcept(Constructor.INTERSECTION, lhs, rhs),
				ConceptName.topConcept());
		if (cd.isNegated()) {
			result.toggleNegated();
		}
		return result;
	}

	private ConceptDefinition primitiveConceptDefinition(ConceptDefinition cd)
			throws CloneNotSupportedException {
		Concept negC = cd.getLhs().toggleNegated();
		Concept D = cd.getRhs();
		BinaryConcept bf = new BinaryConcept(Constructor.UNION, negC, D);
		ConceptDefinition result = new ConceptDefinition(Type.NON_PRIMITIVE,
				bf, ConceptName.topConcept());
		if (cd.isNegated()) {
			result.toggleNegated();
		}
		return result;
	}

}
